Nuprl Lemma : w-a_wf
11,40
postcript
pdf
the_w
:World,
i
:Id,
t
:
. a(
i
;
t
)
Action(
i
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Action(
i
)
,
a(
i
;
t
)
,
w
.TA
,
w
.M
,
t
.1
,
t
.2
,
World
Lemmas
nat
wf
,
Id
wf
,
world
wf
origin
the_w:World, i:Id, t:
. a(i;t) 
Action(i) the_w:World, i:Id, t:. a(i;t) Action(i) x:A. B(x) T